Skip to content

Change arg max to max in Appendix D.#734

Merged
nicksavers merged 1 commit intoethereum:masterfrom
acoglio:arg-max
Mar 28, 2019
Merged

Change arg max to max in Appendix D.#734
nicksavers merged 1 commit intoethereum:masterfrom
acoglio:arg-max

Conversation

@acoglio
Copy link
Member

@acoglio acoglio commented Feb 28, 2019

Here j is the maximum x such that there exists an \mathbf{l} such that etc. etc.
That is, j is the length of the longest common prefix of all the keys (nibble
arrays) of the \mathfrak{I} map.

Note that j is not the argument x that maximizes the value of a function over x.
The expression \exists \mathbf{l} ... following \arg \max is boolean-valued.

Also change a colon into a \wedge, which conjoins the two constraints over x and
\mathbf{l} in the set comprehension.

Here j is the maximum x such that there exists an \mathbf{l} such that etc. etc.
That is, j is the length of the longest common prefix of all the keys (nibble
arrays) of the \mathfrak{I} map.

Note that j is not the argument x that maximizes the value of a function over x.
The expression \exists \mathbf{l} ... following \arg \max is boolean-valued.

Also change a colon into a \wedge, which conjoins the two constraints over x and
\mathbf{l} in the set comprehension.
@nicksavers
Copy link
Contributor

For review. This changes the following

Old formula

into

New formula

@acoglio
Copy link
Member Author

acoglio commented Mar 4, 2019

Thanks, @nicksavers. I'll add screenshots like yours to future PRs.

@acoglio
Copy link
Member Author

acoglio commented Mar 15, 2019

@nicksavers, given that nobody has objected to the change, would you be willing to merge it?

I'll mention that this change is based on a formal specification of Modified Merkle Patricia trees that I have developed in the ACL2 theorem prover, available on GitHub here. In particular, to calculate that index j, I used a max (not arg max) operator, in the function mmp-encode-c-max starting at line 538 of that file. I also proved that the maximum exists, under suitable invariants of the recursive definition of the c and n functions in the Yellow Paper.

@nicksavers nicksavers merged commit dbc2f9b into ethereum:master Mar 28, 2019
@acoglio acoglio deleted the arg-max branch April 11, 2019 23:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants